␈α0␈↓βcommutative␈↓α ␈↓βop␈↓α ← ␈↓βop␈↓α ε (PLUS TIMES UNION INTERSECTION)



␈α0␈↓βinst␈↓α[␈↓βe␈↓α, ␈↓βm␈↓α, ␈↓βp␈↓α] ← 
␈α?␈α⊃␈↓∧if␈↓α ␈↓βp␈↓α ␈↓∧eq ␈↓αNO ␈↓∧then␈↓α ␈↓βp
␈α?␈α⊃␈↓∧else if␈↓α ␈↓∧at ␈↓βm␈↓α ␈↓∧then␈↓α 
␈α?␈α1[␈↓∧if␈↓α ␈↓βisvar␈↓α ␈↓βm␈↓α ␈↓∧then␈↓α 
␈α?␈α?␈α∩{␈↓βassoc␈↓α[␈↓βm␈↓α, ␈↓βp␈↓α]}[λ␈↓βw␈↓α. ␈↓∧if␈↓α ␈↓∧n ␈↓βw␈↓α ␈↓∧then␈↓α [␈↓βm␈↓α . ␈↓βe␈↓α] . ␈↓βp␈↓α ␈↓∧else if␈↓α ␈↓βequal␈↓α[␈↓∧d ␈↓βw␈↓α, ␈↓βe␈↓α] ␈↓∧then␈↓α ␈↓βp␈↓α ␈↓∧else␈↓α NO]
␈α?␈α:␈↓∧else if␈↓α ␈↓βm␈↓α ␈↓∧eq ␈↓βe␈↓α ␈↓∧then␈↓α ␈↓βp
␈α?␈α:␈↓∧else␈↓α NO]
␈α?␈α⊃␈↓∧else if␈↓α ␈↓∧at ␈↓βe␈↓α ␈↓∧then␈↓α NO
␈α?␈α⊃␈↓∧else if␈↓α ␈↓βcommutative␈↓α ␈↓∧a ␈↓βm␈↓α ␈↓∧then␈↓α [␈↓∧if␈↓α ␈↓∧at ␈↓βe␈↓α ␈↓∧then␈↓α NO ␈↓∧else␈↓α ␈↓βcomminst␈↓α[␈↓∧d ␈↓βe␈↓α, ␈↓∧d ␈↓βm␈↓α, ␈↓βinst␈↓α[␈↓∧a ␈↓βe␈↓α, ␈↓∧a ␈↓βm␈↓α, ␈↓βp␈↓α], NIL]]
␈α?␈α⊃␈↓∧else␈↓α ␈↓βinst␈↓α[␈↓∧d ␈↓βe␈↓α, ␈↓∧d ␈↓βm␈↓α, ␈↓βinst␈↓α[␈↓∧a ␈↓βe␈↓α, ␈↓∧a ␈↓βm␈↓α, ␈↓βp␈↓α]]



␈α0␈↓βisvar␈↓α ␈↓βm␈↓α ← ␈↓βm␈↓α ε (U V W X Y Z)



␈α0␈↓βsublis␈↓α[␈↓βe␈↓α, ␈↓βp␈↓α] ← 
␈α?␈α⊃␈↓∧if␈↓α ␈↓∧at ␈↓βe␈↓α ␈↓∧then␈↓α {␈↓βassoc␈↓α[␈↓βe␈↓α, ␈↓βp␈↓α]}[λ␈↓βw␈↓α. ␈↓∧if␈↓α ␈↓∧n ␈↓βw␈↓α ␈↓∧then␈↓α ␈↓βe␈↓α ␈↓∧else␈↓α ␈↓∧d ␈↓βw␈↓α]
␈α?␈α⊃␈↓∧else␈↓α {␈↓βsublis␈↓α[␈↓∧a ␈↓βe␈↓α, ␈↓βp␈↓α], ␈↓βsublis␈↓α[␈↓∧d ␈↓βe␈↓α, ␈↓βp␈↓α]}[λ␈↓βx␈↓α, ␈↓βy␈↓α. ␈↓∧if␈↓α ␈↓βx␈↓α ␈↓∧eq a ␈↓βe␈↓α ∧ ␈↓βy␈↓α ␈↓∧eq d ␈↓βe␈↓α ␈↓∧then␈↓α ␈↓βe␈↓α ␈↓∧else␈↓α ␈↓βx␈↓α . ␈↓βy␈↓α]



␈α0␈↓βcomminst␈↓α[␈↓βlexp␈↓α, ␈↓βlpat␈↓α, ␈↓βa␈↓α, ␈↓βu␈↓α] ← 
␈α?␈α⊃␈↓∧if␈↓α ␈↓βa␈↓α ␈↓∧eq ␈↓αNO ␈↓∧then␈↓α NO
␈α?␈α⊃␈↓∧else if␈↓α ␈↓∧at ␈↓βlpat␈↓α ␈↓∧then␈↓α 
␈α?␈α1[␈↓∧if␈↓α ␈↓βisvar␈↓α ␈↓βlpat␈↓α ␈↓∧then␈↓α 
␈α?␈α?␈α∩{␈↓βassoc␈↓α[␈↓βlpat␈↓α, ␈↓βa␈↓α]}[λ␈↓βw␈↓α. 
␈α?␈α?␈α2␈↓∧if␈↓α ␈↓∧n ␈↓βw␈↓α ␈↓∧then␈↓α [␈↓βlpat␈↓α . [␈↓βlexp␈↓α * ␈↓βu␈↓α]] . ␈↓βa␈↓α ␈↓∧else if␈↓α ␈↓βequal␈↓α[␈↓∧d ␈↓βw␈↓α, ␈↓βlexp␈↓α] ∧ ␈↓∧n ␈↓βu␈↓α ␈↓∧then␈↓α ␈↓βa␈↓α ␈↓∧else␈↓α NO]
␈α?␈α:␈↓∧else if␈↓α ␈↓βlpat␈↓α ␈↓∧eq ␈↓βlexp␈↓α ␈↓∧then␈↓α ␈↓βa
␈α?␈α:␈↓∧else␈↓α NO]
␈α?␈α⊃␈↓∧else if␈↓α ␈↓∧n ␈↓βlexp␈↓α ␈↓∧then␈↓α NO
␈α?␈α⊃␈↓∧else␈↓α {␈↓βinst␈↓α[␈↓∧a ␈↓βlexp␈↓α, ␈↓∧a ␈↓βlpat␈↓α, ␈↓βa␈↓α]}[λ␈↓βw␈↓α. 
␈α?␈α1␈↓∧if␈↓α ␈↓βw␈↓α ␈↓∧eq ␈↓αNO ␈↓∧then␈↓α ␈↓βcomminst␈↓α[␈↓∧d ␈↓βlexp␈↓α, ␈↓βlpat␈↓α, ␈↓βa␈↓α, ␈↓∧a ␈↓βlexp␈↓α . ␈↓βu␈↓α]
␈α?␈α1␈↓∧else␈↓α {␈↓βcomminst␈↓α[␈↓βu␈↓α * ␈↓∧d ␈↓βlexp␈↓α, ␈↓∧d ␈↓βlpat␈↓α, ␈↓βw␈↓α, NIL]}[λ␈↓βz␈↓α. 
␈α?␈α?␈α∩␈↓∧if␈↓α ␈↓βz␈↓α ␈↓∧eq ␈↓αNO ␈↓∧then␈↓α ␈↓βcomminst␈↓α[␈↓∧d ␈↓βlexp␈↓α, ␈↓βlpat␈↓α, ␈↓βa␈↓α, ␈↓∧a ␈↓βlexp␈↓α . ␈↓βu␈↓α] ␈↓∧else␈↓α ␈↓βz␈↓α]]